|
In intuitionistic type theory (ITT), a discipline within mathematical logic, induction-recursion is a feature for simultaneously declaring a type and function on that type. It allows the creation of larger types, such as universes, than inductive types. The types created still remain predicative inside ITT. An inductive definition is given by rules for generating elements of a type. One can then define functions from that type by induction on the way the elements of the type are generated. Induction-recursion generalizes this situation since one can ''simultaneously'' define the type and the function, because the rules for generating elements of the type are allowed to refer to the function. Induction-recursion can be used to define large types including various universe constructions. It increases the proof-theoretic strength of type theory substantially. Nevertheless, inductive-recursive recursive definitions are still considered predicative. ==Background== Induction-Recursion came out of investigations to the rules of Martin-Löf's intuitionistic type theory. The type theory has a number of "type formers" and 4 kinds rules for each one. Martin-Löf had hinted that the rules for each type former followed a pattern, which preserved the properties of the type theory (e.g., strong normalization, predicativity). Researchers started looking for the most general description of the pattern, since that would tell what kinds of type formers could be added (or not added!) to extend the type theory. The "universe" type former was the most interesting, because when the rules were written "ala Tarski", they simultaneously defined the "universe type" ''and ''a function that operated on it. This eventually lead Dybjer to Induction-Recursion. Dybjer's initial papers called Induction-Recursion a "schema" for rules. It stated what type formers could be added to the type theory. Later, he and Setzer would write a new type former with rules that allowed new Induction-Recursion definitions to be made inside the type theory. This was added to the Half proof assistant (a variant of Alf). 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Induction-recursion (type theory)」の詳細全文を読む スポンサード リンク
|